Require Export Matrix.Mat.Matrix_Module.


(* the height of a two-dimensional list *)
Check height. (* list (list ?A) -> nat where ?A : [ |- Set] *)

(* the width of a two-dimensional list *)
Check width. (* list (list ?A) -> nat -> Prop where ?A : [ |- Set] *)

(* make a matrix *)
Check mkMat: forall (A : Set) (m n : nat)(mat : list (list A)),
        height mat = m -> width mat n -> Mat A m n.

Check M_eq. (* Mat ?A ?m ?n -> Mat ?A ?m ?n -> Prop. Notation: === *)

Print "===".

(* Zero matrix *)
Check MO:forall A : Set, A -> forall m n : nat, Mat A m n.

(* One matrix *)
Check MI:forall A : Set, A -> A -> forall n : nat, Mat A n n.

(* A +/- B *)
Check matrix_each : forall A : Set, (A -> A -> A) -> forall m n : nat, 
        Mat A m n -> Mat A m n -> Mat A m n.
(* - A *)
Check matrix_map : forall A : Set, (A -> A) -> forall m n : nat,
        Mat A m n -> Mat A m n.

(* A + B === B + A *)
Check matrix_comm:forall (A : Set) (add : A -> A -> A) (m n : nat) (left right : Mat A m n),
       (forall a b : A, add a b = add b a) ->
       matrix_each A add left right === matrix_each A add right left.

(* A + B + C === A + ( B + C ) *)
Check matrix_assoc:forall (A : Set) (add : A -> A -> A) (m n : nat) (left middle right : Mat A m n),
       (forall a b c : A, add (add a b) c = add a (add b c)) ->
       matrix_each A add (matrix_each A add left middle) right ===
       matrix_each A add left (matrix_each A add middle right).

(* O + A === A, where O is a zero matrix *)
Check matrix_add_zero_l : forall (A : Set) (Zero : A) (add : A -> A -> A) (m n : nat) (ma : Mat A m n),
       (forall a : A, add Zero a = a) -> matrix_each A add (MO A Zero m n) ma === ma.

(* A + O === A *)
Check matrix_add_zero_r : forall (A : Set) (Zero : A) (add : A -> A -> A) (m n : nat) (ma : Mat A m n),
       (forall a : A, add a Zero = a) -> matrix_each A add ma (MO A Zero m n) === ma.

(* A === B && C === D -> A +/- C === B +/- D *)
Check matrix_each_compat: forall (A : Set) (f : A -> A -> A) 
      (m n : nat) (x x' : Mat A m n), x === x' ->
       forall y y' : Mat A m n, y === y' -> matrix_each A f x y === matrix_each A f x' y'.

(* A === B -> - A === - B *)
Check matrix_map_compat : forall (A : Set) (f : A -> A) (m n : nat) (x x' : Mat A m n),
       x === x' -> matrix_map A f x === matrix_map A f x'.

(* A - B === - ( B - A) *) 
Check matrix_sub_opp : forall (A : Set) (negative : A -> A) (sub : A -> A -> A) (m n : nat)
         (ma1 ma2 : Mat A m n),
       (forall a b : A, sub a b = negative (sub b a)) ->
       matrix_each A sub ma1 ma2 === matrix_map A negative (matrix_each A sub ma2 ma1).

(* A - B - C === A - ( B + C) *)
Check matrix_sub_assoc : forall (A : Set) (add sub : A -> A -> A) (m n : nat) (mat1 mat2 mat3 : Mat A m n),
       (forall a b c : A, sub (sub a b) c = sub a (add b c)) ->
       matrix_each A sub (matrix_each A sub mat1 mat2) mat3 ===
       matrix_each A sub mat1 (matrix_each A add mat2 mat3).

(* O - A === - A *)
Check matrix_sub_zero_l : forall (A : Set) (Zero : A) (negative : A -> A) (sub : A -> A -> A) 
         (m n : nat) (ma : Mat A m n),
       (forall a : A, sub Zero a = negative a) ->
       matrix_each A sub (MO A Zero m n) ma === matrix_map A negative ma.

(* A - O === A *)
Check matrix_sub_zero_r : forall (A : Set) (Zero : A) (sub : A -> A -> A) (m n : nat) (ma : Mat A m n),
       (forall a : A, sub a Zero = a) -> matrix_each A sub ma (MO A Zero m n) === ma.

(* A - A === O *)
Check matrix_sub_self  : forall (A : Set) (Zero : A) (sub : A -> A -> A) (m n : nat) (ma : Mat A m n),
       (forall a : A, sub a a = Zero) -> matrix_each A sub ma ma === MO A Zero m n.

(* transpose of matrix : T(A) *)
Check trans : forall A : Set, A -> forall m n : nat, Mat A m n -> Mat A n m.

(* T(T(A)) === A *)
Check tteq  : forall (A : Set) (Zero : A) (m n : nat) (ma : Mat A m n),
       trans A Zero (trans A Zero ma) === ma.

(* T(I) === I , where I is a unit matrix *)
Check trans_MI : forall (A : Set) (Zero One : A) (n : nat),
       trans A Zero (MI A Zero One n) === MI A Zero One n.

(* A === B -> T(A) === T(B) *)
Check trans_compat : forall (A : Set) (Zero : A) (m n : nat) (x x' : Mat A m n),
       x === x' -> trans A Zero x === trans A Zero x'.

(* A × B (need zero,add and mul as its arguments *)
Check matrix_mul : forall A : Set,
       A ->(A -> A -> A) ->(A -> A -> A) -> 
    forall m n p : nat, Mat A m n -> Mat A n p -> Mat A m p.

(* A === B && C === D -> A × B === C × D *)
Check matrix_mul_compat : forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p : nat) (x x' : Mat A m n),
       x === x' -> forall y y' : Mat A n p,
       y === y' -> matrix_mul A Zero add mul x y === matrix_mul A Zero add mul x' y'.

(* k * A , where k has the same type as the elements in A *)
Check const_mul_l : forall A : Set, (A -> A -> A) -> 
    forall m n : nat, A -> Mat A m n -> Mat A m n.

(* A * k , where k has the same type as the elements in A *)
Check const_mul_r: forall A : Set, (A -> A -> A) -> 
    forall m n : nat, A -> Mat A m n -> Mat A m n.

(* ( A +/- B ) × C === A × C +/- B × C *)
Check matrix_mul_distr_l  : forall (A : Set) (Zero : A) (add mul f : A -> A -> A) (m n p : nat) 
         (a b : Mat A m n) (c : Mat A n p),
       (forall a0 : A, f a0 Zero = a0) ->
       (forall a0 b0 c0 d : A, f (add a0 b0) (add c0 d) = add (f a0 c0) (f b0 d)) ->
       (forall a0 b0 c0 : A, mul (f a0 b0) c0 = f (mul a0 c0) (mul b0 c0)) ->
       matrix_mul A Zero add mul (matrix_each A f a b) c ===
       matrix_each A f (matrix_mul A Zero add mul a c) (matrix_mul A Zero add mul b c).

(* A × ( B +/- C) === A × B +/- A × C *)
Check matrix_mul_distr_r : forall (A : Set) (Zero : A) (add mul f : A -> A -> A) (m n p : nat) 
         (a : Mat A m n) (b c : Mat A n p),
       (forall a0 : A, f a0 Zero = a0) ->
       (forall a0 b0 c0 d : A, f (add a0 b0) (add c0 d) = add (f a0 c0) (f b0 d)) ->
       (forall a0 b0 c0 : A, mul a0 (f b0 c0) = f (mul a0 b0) (mul a0 c0)) ->
       matrix_mul A Zero add mul a (matrix_each A f b c) ===
       matrix_each A f (matrix_mul A Zero add mul a b) (matrix_mul A Zero add mul a c).

(* O × A === O *) 
Check matrix_mul_zero_l : forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p : nat) (ma : Mat A n p),
       (forall a : A, mul Zero a = Zero) ->
       (forall a : A, add Zero a = a) ->
       matrix_mul A Zero add mul (MO A Zero m n) ma === MO A Zero m p.

(* A × O === O *)
Check matrix_mul_zero_r : forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p : nat) (ma : Mat A m n),
       (forall a b : A, mul a b = mul b a) ->
       (forall a0 : A, mul a0 Zero = Zero) ->
       (forall a0 : A, add Zero a0 = a0) ->
       matrix_mul A Zero add mul ma (MO A Zero n p) === MO A Zero m p.

(* A × B × C === A × ( B × C ) *)
Check matrix_mul_assoc :forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p k : nat) 
         (a : Mat A m n) (b : Mat A n p) (c : Mat A p k),
       (forall a0 : A, add a0 Zero = a0) ->
       (forall a0 b0 c0 : A, mul (mul a0 b0) c0 = mul a0 (mul b0 c0)) ->
       (forall a0 : A, mul a0 Zero = Zero) ->
       (forall a0 : A, mul Zero a0 = Zero) ->
       (forall a0 : A, add Zero a0 = a0) ->
       (forall a0 b0 c0 : A, mul a0 (add b0 c0) = add (mul a0 b0) (mul a0 c0)) ->
       (forall a0 b0 : A, mul a0 b0 = mul b0 a0) ->
       (forall a0 b0 c0 : A, mul (add a0 b0) c0 = add (mul a0 c0) (mul b0 c0)) ->
       (forall a0 b0 c0 d : A, add (add a0 b0) (add c0 d) = add (add a0 c0) (add b0 d)) ->
       matrix_mul A Zero add mul (matrix_mul A Zero add mul a b) c ===
       matrix_mul A Zero add mul a (matrix_mul A Zero add mul b c).

(* k * A = A * k *)
Check c_mul_l_comm  : forall (A : Set) (mul : A -> A -> A) (c : A) (l : list A),
       (forall a b : A, mul a b = mul b a) -> c_mul_l A mul c l = l_mul_c A mul c l.

(* ( k1 +/- k2 ) * A === k1 * A +/- k2 * A *)
Check const_mul_l_distr_l: forall (A : Set) (add mul : A -> A -> A) (m n : nat) (c1 c2 : A) (ma : Mat A m n),
       (forall a b c : A, mul (add a b) c = add (mul a c) (mul b c)) ->
       const_mul_l A mul (add c1 c2) ma ===
       matrix_each A add (const_mul_l A mul c1 ma) (const_mul_l A mul c2 ma).

(* k * ( A +/- B ) === k * A +/- k * B *) 
Check const_mul_l_distr_r : forall (A : Set) (add mul : A -> A -> A) (m n : nat) (c : A) (ma1 ma2 : Mat A m n),
       (forall a b c0 : A, mul a (add b c0) = add (mul a b) (mul a c0)) ->
       const_mul_l A mul c (matrix_each A add ma1 ma2) ===
       matrix_each A add (const_mul_l A mul c ma1) (const_mul_l A mul c ma2).

(* 0 * A === O *)
Check const_mul_l_0: forall (A : Set) (Zero : A) (mul : A -> A -> A) (m n : nat) (ma : Mat A m n),
       (forall a : A, mul Zero a = Zero) -> const_mul_l A mul Zero ma === MO A Zero m n.


(* A * 0 === O *)
Check const_mul_r_0: forall (A : Set) (Zero : A) (mul : A -> A -> A) (m n : nat) (ma : Mat A m n),
       (forall a : A, mul Zero a = Zero) -> (forall a b : A, mul a b = mul b a) ->
      const_mul_r A mul Zero ma === MO A Zero m n.

(* T(k*A) === k * T(A) *)
Check cteq : forall (A : Set) (Zero : A) (mul : A -> A -> A) (m n : nat) (c : A) (ma : Mat A m n),
       (forall a : A, mul a Zero = Zero) ->
       trans A Zero (const_mul_l A mul c ma) === const_mul_l A mul c (trans A Zero ma).
 
(* O × A === O *)
Check matrix_mul_zero_l: forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p : nat) (ma : Mat A n p),
       (forall a : A, mul Zero a = Zero) ->
       (forall a : A, add Zero a = a) ->
       matrix_mul A Zero add mul (MO A Zero m n) ma === MO A Zero m p.

(* A × O === O *)
Check matrix_mul_zero_r: forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p : nat) (ma : Mat A m n),
       (forall a b : A, mul a b = mul b a) ->
       (forall a0 : A, mul a0 Zero = Zero) ->
       (forall a0 : A, add Zero a0 = a0) ->
       matrix_mul A Zero add mul ma (MO A Zero n p) === MO A Zero m p.

(* I * A === I , where I is a unit matrix *)
Check matrix_mul_unit_l : forall (A : Set) (Zero One : A) (add mul : A -> A -> A) (m n : nat) (ma : Mat A m n),
       (forall a : A, mul One a = a) ->
       (forall a : A, add a Zero = a) ->
       (forall a : A, mul Zero a = Zero) ->
       (forall a : A, add Zero a = a) ->
       matrix_mul A Zero add mul (MI A Zero One m) ma === ma.

(* A * I === A *)
Check matrix_mul_unit_r : forall (A : Set) (Zero : A) (add mul : A -> A -> A) (One : A) 
         (m n : nat) (ma : Mat A m n),
       (forall a : A, mul One a = a) ->
       (forall a : A, add a Zero = a) ->
       (forall a : A, mul Zero a = Zero) ->
       (forall a : A, add Zero a = a) ->
       (forall a b : A, mul a b = mul b a) ->
       matrix_mul A Zero add mul ma (MI A Zero One n) === ma.

(* T ( A + B ) === T(A) + T(B) *)
Check teq_add : forall (A : Set) (Zero : A) (add : A -> A -> A) (m n : nat) (ma mb : Mat A m n),
       (forall a : A, add a Zero = a) ->
       trans A Zero (matrix_each A add ma mb) ===
       matrix_each A add (trans A Zero ma) (trans A Zero mb).

(* T( A × B ) === T(B)*T(A) *)
Check teq_mul : forall (A : Set) (Zero : A) (add mul : A -> A -> A) (m n p : nat) 
         (ma : Mat A m n) (mb : Mat A n p),
       (forall a : A, add Zero a = a) ->
       (forall a b : A, mul a b = mul b a) ->
       trans A Zero (matrix_mul A Zero add mul ma mb) ===
       matrix_mul A Zero add mul (trans A Zero mb) (trans A Zero ma).

End Matrix.



















